#! awk
# Number all lines
{
  printf( "%8d ",  ++line );
  print;
}